perm filename SCHEMA[1,JRA] blob sn#005857 filedate 1972-07-21 generic text, type T, neo UTF8
00100	∀(X2 X3)(((∀(X1)((LE(ADD1(X2) X1) ∧ LE(X1 X3))→α(X1)) ∧ LE(X2 X3)) →α(X2))
00200	  → ∀(X1)((LE(X2 X1) ∧ LE(X1 X3) )→ α(X1)));